Bob is cold. Charlie is blue. Dave is rough. Erin is round. If someone is red then they are blue. If Bob is furry and Bob is round then Bob is blue. If someone is cold then they are blue. Smart people are cold. If Dave is blue and Dave is cold then Dave is furry. Blue people are round. If Bob is round then Bob is smart. If someone is red then they are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Bob is furry and Bob is round then Bob is blue.
((("Bob" "is" "furry" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "blue" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Dave is blue and Dave is cold then Dave is furry.
((("Dave" "is" "blue" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "furry" "+"))
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Bob is round then Bob is smart.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "smart" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Erin is round.
True
1
proof
[(triple4)]
("Erin" "is" "round" "+")
triple4
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Dave is not round.
Unknown
inv-rconc
[@4: Dave is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- rule8 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is cold.[(triple1)] Charlie is blue.[(triple2)] Dave is rough.[(triple3)] Erin is round.[(triple4)] @1: Bob is blue.[(((triple1) -> rule3))] Charlie is round.[(((triple2) -> rule6))] @2: Bob is round.[(((((triple1) -> rule3)) -> rule6))] @3: Bob is smart.[(((((((triple1) -> rule3)) -> rule6)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3