Fiona is big. Fiona is cold. Fiona is smart. Harry is kind. Harry is quiet. Harry is red. Harry is smart. Round people are big. If Harry is big and Harry is smart then Harry is round. All cold, smart people are kind. If someone is red and not cold then they are quiet. Kind people are red. All quiet people are smart.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If Harry is big and Harry is smart then Harry is round.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "round" "+"))
All cold, smart people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not cold then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "+"))
Kind people are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple7 OR ((triple5) -> rule6))]
("Harry" "is" "smart" "+")
triple7
((triple5) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Fiona is not smart.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Fiona is kind.
True
3
proof
[(((triple2 triple3) -> rule3))]
("Fiona" "is" "kind" "+")
((triple2 triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
3
inv-proof
[(((triple2 triple3) -> rule3))]
("Fiona" "is" "kind" "-")
((triple2 triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
True
4
proof
[(((((triple2 triple3) -> rule3)) -> rule5))]
("Fiona" "is" "red" "+")
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not red.
False
4
inv-proof
[(((((triple2 triple3) -> rule3)) -> rule5))]
("Fiona" "is" "red" "-")
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Fiona is big.[(triple1)] Fiona is cold.[(triple2)] Fiona is smart.[(triple3)] Harry is kind.[(triple4)] Harry is quiet.[(triple5)] Harry is red.[(triple6 OR ((triple4) -> rule5))] Harry is smart.[(triple7 OR ((triple5) -> rule6))] @1: Fiona is kind.[(((triple2 triple3) -> rule3))] @2: Fiona is red.[(((((triple2 triple3) -> rule3)) -> rule5))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
((triple4) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
((triple5) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple2 triple3) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2