Bob is smart. Dave is green. Gary is smart. Harry is smart. If Gary is green and Gary is white then Gary is red. White people are round. All smart people are white. Green people are smart. All round people are green. If Bob is cold and Bob is round then Bob is red.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Gary is green and Gary is white then Gary is red.
((("Gary" "is" "green" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "red" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Bob is cold and Bob is round then Bob is red.
((("Bob" "is" "cold" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "red" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Bob is white.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "white" "-")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is round.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Harry" "is" "round" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is green.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is smart.[(triple1)] Dave is green.[(triple2)] Gary is smart.[(triple3)] Harry is smart.[(triple4)] @1: Bob is white.[(((triple1) -> rule3))] Dave is smart.[(((triple2) -> rule4))] Gary is white.[(((triple3) -> rule3))] Harry is white.[(((triple4) -> rule3))] @2: Bob is round.[(((((triple1) -> rule3)) -> rule2))] Dave is white.[(((((triple2) -> rule4)) -> rule3))] Gary is round.[(((((triple3) -> rule3)) -> rule2))] Harry is round.[(((((triple4) -> rule3)) -> rule2))] @3: Bob is green.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))] Dave is round.[(((((((triple2) -> rule4)) -> rule3)) -> rule2))] Gary is green.[(((((((triple3) -> rule3)) -> rule2)) -> rule5))] Harry is green.[(((((((triple4) -> rule3)) -> rule2)) -> rule5))] @4: Gary is red.[(((((((((triple3) -> rule3)) -> rule2)) -> rule5) ((triple3) -> rule3)) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int4))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4