Bob is smart. Dave is round. Gary is round. Harry is rough. If Gary is smart then Gary is round. All big things are blue. If something is cold and smart then it is big. Red things are big. If Dave is rough and Dave is not cold then Dave is round. If Harry is not rough then Harry is big. If Bob is smart and Bob is round then Bob is not red. If something is smart then it is round.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is smart then Gary is round.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "round" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is cold and smart then it is big.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Dave is rough and Dave is not cold then Dave is round.
((("Dave" "is" "rough" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "round" "+"))
If Harry is not rough then Harry is big.
((("Harry" "is" "rough" "~")) -> ("Harry" "is" "big" "+"))
If Bob is smart and Bob is round then Bob is not red.
((("Bob" "is" "smart" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "red" "-"))
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Bob is round.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "-")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not red.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule7))]
("Bob" "is" "red" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule7))]
("Bob" "is" "red" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "blue" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is round.[(triple2)] Gary is round.[(triple3)] Harry is rough.[(triple4)] @1: Bob is round.[(((triple1) -> rule8))] @2: Bob is not red.[(((triple1 ((triple1) -> rule8)) -> rule7))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not red.
("Bob" "is" "red" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2