Bob is green. Charlie is green. Fiona is big. Fiona is cold. Fiona is rough. Harry is cold. Harry is round. Quiet, green people are furry. All green, furry people are big. If Bob is green then Bob is quiet.
Bob is green.
("Bob" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Quiet, green people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All green, furry people are big.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If Bob is green then Bob is quiet.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Harry is not cold.
False
1
inv-proof
[(triple6)]
("Harry" "is" "cold" "-")
triple6
Bob is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is green.[(triple1)] Charlie is green.[(triple2)] Fiona is big.[(triple3)] Fiona is cold.[(triple4)] Fiona is rough.[(triple5)] Harry is cold.[(triple6)] Harry is round.[(triple7)] @1: Bob is quiet.[(((triple1) -> rule3))] @2: Bob is furry.[(((((triple1) -> rule3) triple1) -> rule1))] @3: Bob is big.[(((triple1 ((((triple1) -> rule3) triple1) -> rule1)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple1 ((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3