Bob is not rough. Charlie is rough. Fiona is smart. Harry is smart. All rough people are smart. Kind people are blue. If someone is smart then they are not white. If Harry is big then Harry is not blue. If Harry is nice then Harry is big. If Harry is not white then Harry is big.
Bob is not rough.
("Bob" "is" "rough" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are not white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
If Harry is big then Harry is not blue.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "-"))
If Harry is nice then Harry is big.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "big" "+"))
If Harry is not white then Harry is big.
((("Harry" "is" "white" "~")) -> ("Harry" "is" "big" "+"))
Harry is smart.
True
1
proof
[(triple4)]
("Harry" "is" "smart" "+")
triple4
Bob is rough.
False
1
inv-proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Charlie is smart.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not white.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Harry is not blue.
True
4
proof
[(((((((triple4) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "blue" "-")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3
Harry is blue.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "blue" "+")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is not rough.[(triple1)] Charlie is rough.[(triple2)] Fiona is smart.[(triple3)] Harry is smart.[(triple4)] @1: Charlie is smart.[(((triple2) -> rule1))] Fiona is not white.[(((triple3) -> rule3))] Harry is not white.[(((triple4) -> rule3))] @2: Charlie is not white.[(((((triple2) -> rule1)) -> rule3))] Harry is big.[(((((triple4) -> rule3)) -> rule6))] @3: Harry is not blue.[(((((((triple4) -> rule3)) -> rule6)) -> rule4))]
Bob is not rough.
("Bob" "is" "rough" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not white.
("Fiona" "is" "white" "-")
((triple3) -> (rule3 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple4) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Charlie is not white.
("Charlie" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
int2
Harry is not blue.
("Harry" "is" "blue" "-")
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not white.
("Harry" "is" "white" "-")
int3