Bob is big. Bob is smart. Bob is white. Charlie is big. Charlie is blue. Charlie is green. Charlie is smart. Charlie is white. Dave is big. Dave is green. Dave is white. Harry is big. Harry is blue. Harry is green. Harry is smart. If Bob is big then Bob is blue. Green people are big. If someone is green and big then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Bob is big then Bob is blue.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "blue" "+"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is green and big then they are white.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Dave is big.
True
1
proof
[(triple9 OR ((triple10) -> rule2))]
("Dave" "is" "big" "+")
triple9
((triple10) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is blue.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Charlie is big.[(triple4 OR ((triple6) -> rule2))] Charlie is blue.[(triple5)] Charlie is green.[(triple6)] Charlie is smart.[(triple7)] Charlie is white.[(triple8 OR ((triple6 triple4) -> rule3) OR ((triple6 ((triple6) -> rule2)) -> rule3))] Dave is big.[(triple9 OR ((triple10) -> rule2))] Dave is green.[(triple10)] Dave is white.[(triple11 OR ((triple10 triple9) -> rule3) OR ((triple10 ((triple10) -> rule2)) -> rule3))] Harry is big.[(triple12 OR ((triple14) -> rule2))] Harry is blue.[(triple13)] Harry is green.[(triple14)] Harry is smart.[(triple15)] @1: Bob is blue.[(((triple1) -> rule1))] Harry is white.[(((triple14 triple12) -> rule3) OR ((triple14 ((triple14) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple6) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple6 triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple6 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple9
((triple10) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple10 triple9) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple10 ((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple12
((triple14) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple14 triple12) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple14 ((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2