Bob is big. Dave is blue. Round things are white. All rough, big things are nice. Round, blue things are big. All blue things are green. If something is blue and green then it is rough. All rough, green things are big.
Bob is big.
("Bob" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All rough, big things are nice.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Round, blue things are big.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is blue and green then it is rough.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All rough, green things are big.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is green.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "green" "-")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "green" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1)] Dave is blue.[(triple2)] @1: Dave is green.[(((triple2) -> rule4))] @2: Dave is rough.[(((triple2 ((triple2) -> rule4)) -> rule5))] @3: Dave is big.[(((((triple2 ((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule6))] @4: Dave is nice.[(((((triple2 ((triple2) -> rule4)) -> rule5) ((((triple2 ((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule6)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2 ((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple2 ((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4